package com.tressatisfiability.shared;

import java.io.Serializable;
import java.util.Stack;

import com.google.gwt.user.client.ui.HTML;

public class Formula implements Serializable {

	private static final long serialVersionUID = 9115878519648992494L;
	private Stack<Clausula> clausulas;
	private boolean satisfied;
	private int nvariables;
	private boolean variables[];

	private Formula() {
		super();
		clausulas = new Stack<Clausula>();
	}

	public Formula(String s) {
		clausulas = new Stack<Clausula>();
		while (s.contains("#")) {
			String u = "";
			for (int i = s.indexOf("#"); i < s.length(); i++) {
				if (s.charAt(i) == '\n') {
					u += s.charAt(i);
					s = s.replace(u, "");
					break;
				} else {
					u += s.charAt(i);
				}
			}
		}
		while (s.endsWith("\n")) {
			s = s.substring(0, s.length() - 1);
		}

		nvariables = Integer.parseInt(s.substring(0, s.indexOf(" ")));
		s = s.replaceFirst(s.substring(0, s.indexOf("\n") + 1), "");
		variables = new boolean[nvariables];

		while (s.length() > 0) {
			String ss;
			if (s.contains("\n")) {
				ss = s.substring(0, s.indexOf("\n"));
				s = s.replace(ss + "\n", "");
			} else {
				ss = s;
				s = "";
			}

			int v1 = Integer.parseInt(ss.substring(0, ss.indexOf(" ")));
			ss = ss.replaceFirst(ss.substring(0, ss.indexOf(" ") + 1), "");
			int v2 = Integer.parseInt(ss.substring(0, ss.indexOf(" ")));
			ss = ss.replaceFirst(ss.substring(0, ss.indexOf(" ") + 1), "");
			int v3 = Integer.parseInt(ss.trim());
			clausulas.push(new Clausula(v1, v2, v3, false, false, false));
		}
		randomVariables();
		reEvaluate();
	}

	private void reEvaluate() {
		satisfied = true;
		for (Clausula c : clausulas) {
			if (!c.isSatisfied()) {
				satisfied = false;
				break;
			}
		}
	}

	public Stack<Clausula> getClausulas() {
		return clausulas;
	}

	public boolean isSatisfied() {
		return satisfied;
	}

	// public void flipVariable(int v) {
	// if (variables[v - 1]) {
	// variables[v - 1] = false;
	// } else {
	// variables[v - 1] = true;
	// }
	// for (Clausula c : clausulas) {
	// c.flipVariable(v);
	// }
	// }
	public void flipVariable(int v) {
		for (Clausula c : clausulas) {
			c.flipVariable(v);
		}
	}

	private void randomVariables() {
		for (int i = 0; i < nvariables; i++) {
			variables[i] = Random.randomBoolean();
			for (Clausula c : clausulas) {
				c.setVariableValue(i + 1, variables[i]);
			}
		}
	}

	private Stack<Clausula> getUnSatisfiedClauses() {
		Stack<Clausula> retorno = new Stack<Clausula>();
		for (Clausula c : clausulas) {
			if (!c.isSatisfied()) {
				retorno.push(c);
			}
		}
		return retorno;
	}

//	public void solve() {
//		int n, m = clausulas.size() * 4;
//		for (n = 0; n < m; n++) {
//			if (isSatisfied()) {
//				return;
//			} else {
//				int clausula;
//				Clausula c;
//				do {
//					clausula = Random.randomInt(clausulas.size());
//					c = clausulas.get(clausula);
//				} while (c.isSatisfied());
//				int variable = Random.randomInt(3);
//				int var = Math.abs(c.getVariables()[variable]);
//				flipVariable(var);
//				reEvaluate();
//			}
//		}
//	}

	public void solve() {
		int n, m = clausulas.size() * 4;
		for (n = 0; n < m; n++) {
			if (isSatisfied()) {
				return;
			} else {
				Stack<Clausula> un = getUnSatisfiedClauses();
				int clausula = Random.randomInt(un.size());
				int variable = Random.randomInt(3);
				variables[Math.abs(un.get(clausula).getVariables()[variable]) - 1] = !variables[Math
						.abs(un.get(clausula).getVariables()[variable]) - 1];
				flipVariable(Math
						.abs(un.get(clausula).getVariables()[variable]));
				reEvaluate();
			}
		}
	}

	@Override
	public String toString() {
		String s = "";
		for (int i = 0; i < clausulas.size(); i++) {
			s += clausulas.get(i).toHTML();
			if (i < clausulas.size() - 1) {
				s += " ^ ";
			}
		}
		return s;
	}

	public HTML getVariablesHTML() {
		String s = "";
		for (int i = 0; i < nvariables; i++) {
			s += "x<sub>";
			s += (i + 1);
			s += "</sub> = ";
			s += variables[i];
			s += "<div>";
		}
		return new HTML(s);
	}

	public String toStringVariables() {
		String s = "";
		for (int i = 0; i < nvariables; i++) {
			s += "x";
			s += (i + 1);
			s += " = ";
			s += variables[i];
			s += "\n";
		}
		return s;
	}

}
